

LEMMA

If x partially overlaps y and y is a tangential proper part of z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (po c980409 c980408)) v (~ (tpp c980408 c980407))) v (~ (p c980407 c980409)))


> hypdisj
=============================
Step 3

? (~ (p c980407 c980409))

1. (tpp c980408 c980407)
2. (po c980409 c980408)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var43 c980407)
|
|1. (p c980407 c980409)
|2. (tpp c980408 c980407)
|3. (po c980409 c980408)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var46 c980407)
||
||1. (~ (c Var43 c980407))
||2. (p c980407 c980409)
||3. (tpp c980408 c980407)
||4. (po c980409 c980408)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 6
||
||? (pp Var46 c980407)
||
||1. (~ (p Var46 c980407))
||2. (~ (c Var43 c980407))
||3. (p c980407 c980409)
||4. (tpp c980408 c980407)
||5. (po c980409 c980408)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 7
||
||? (tpp Var46 c980407)
||
||1. (~ (pp Var46 c980407))
||2. (~ (p Var46 c980407))
||3. (~ (c Var43 c980407))
||4. (p c980407 c980409)
||5. (tpp c980408 c980407)
||6. (po c980409 c980408)
||
||> hyp
|=============================
|Step 8
|
|? (c (f975356 c980408 Var55 Var56) c980408)
|
|1. (~ (c (f975356 c980408 Var55 Var56) c980407))
|2. (p c980407 c980409)
|3. (tpp c980408 c980407)
|4. (po c980409 c980408)
|
|> ((c (f975356 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p c980408 Var55))
|
|1. (~ (c (f975356 c980408 Var55 Var56) c980408))
|2. (~ (c (f975356 c980408 Var55 Var56) c980407))
|3. (p c980407 c980409)
|4. (tpp c980408 c980407)
|5. (po c980409 c980408)
|
|> ((~ (p Y X)) <-- (po X Y))
|=============================
|Step 10
|
|? (po Var55 c980408)
|
|1. (p c980408 Var55)
|2. (~ (c (f975356 c980408 Var55 Var56) c980408))
|3. (~ (c (f975356 c980408 Var55 Var56) c980407))
|4. (p c980407 c980409)
|5. (tpp c980408 c980407)
|6. (po c980409 c980408)
|
|> hyp
=============================
Step 11

? (~ (c (f975356 c980408 c980409 Var56) c980409))

1. (p c980407 c980409)
2. (tpp c980408 c980407)
3. (po c980409 c980408)

> ((~ (c (f975356 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 12

? (~ (p c980408 c980409))

1. (c (f975356 c980408 c980409 Var56) c980409)
2. (p c980407 c980409)
3. (tpp c980408 c980407)
4. (po c980409 c980408)

> ((~ (p Y X)) <-- (po X Y))
=============================
Step 13

? (po c980409 c980408)

1. (p c980408 c980409)
2. (c (f975356 c980408 c980409 Var56) c980409)
3. (p c980407 c980409)
4. (tpp c980408 c980407)
5. (po c980409 c980408)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c985638 c985637)) v (o c985638 c985637))


> hypdisj
=============================
Step 3

? (o c985638 c985637)

1. (po c985638 c985637)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c985638 c985637)

1. (~ (o c985638 c985637))
2. (po c985638 c985637)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c990923 c990922)) v (c c990923 c990922))


> hypdisj
=============================
Step 3

? (c c990923 c990922)

1. (o c990923 c990922)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c990922)
|
|1. (~ (c c990923 c990922))
|2. (o c990923 c990922)
|
|> ((p Z X) <-- (~ (c (f985670 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f985670 Var48 c990922 Var51) Var48))
|
|1. (~ (p Var48 c990922))
|2. (~ (c c990923 c990922))
|3. (o c990923 c990922)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f985687 Var57 Var54) Var54)
||
||1. (c (f985670 (f985687 Var57 Var54) c990922 Var51) (f985687 Var57 Var54))
||2. (~ (p (f985687 Var57 Var54) c990922))
||3. (~ (c c990923 c990922))
||4. (o c990923 c990922)
||
||> ((p (f985687 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f985687 Var57 Var54) Var54))
||2. (c (f985670 (f985687 Var57 Var54) c990922 Var51) (f985687 Var57 Var54))
||3. (~ (p (f985687 Var57 Var54) c990922))
||4. (~ (c c990923 c990922))
||5. (o c990923 c990922)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f985670 (f985687 c990923 c990922) c990922 Var51) c990922))
|
|1. (c (f985670 (f985687 c990923 c990922) c990922 Var51) (f985687 c990923 c990922))
|2. (~ (p (f985687 c990923 c990922) c990922))
|3. (~ (c c990923 c990922))
|4. (o c990923 c990922)
|
|> ((~ (c (f985670 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f985687 c990923 c990922) c990922))
|
|1. (c (f985670 (f985687 c990923 c990922) c990922 Var51) c990922)
|2. (c (f985670 (f985687 c990923 c990922) c990922 Var51) (f985687 c990923 c990922))
|3. (~ (p (f985687 c990923 c990922) c990922))
|4. (~ (c c990923 c990922))
|5. (o c990923 c990922)
|
|> hyp
=============================
Step 10

? (c c990923 (f985687 c990923 c990922))

1. (~ (c c990923 c990922))
2. (o c990923 c990922)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f985687 c990923 c990922) c990923)

1. (~ (c c990923 (f985687 c990923 c990922)))
2. (~ (c c990923 c990922))
3. (o c990923 c990922)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f985687 c990923 Var71) c990923)
|
|1. (~ (c (f985687 c990923 c990922) c990923))
|2. (~ (c c990923 (f985687 c990923 c990922)))
|3. (~ (c c990923 c990922))
|4. (o c990923 c990922)
|
|> ((p (f985687 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c990923 Var71)
|
|1. (~ (p (f985687 c990923 Var71) c990923))
|2. (~ (c (f985687 c990923 c990922) c990923))
|3. (~ (c c990923 (f985687 c990923 c990922)))
|4. (~ (c c990923 c990922))
|5. (o c990923 c990922)
|
|> hyp
=============================
Step 14

? (c (f985687 c990923 c990922) (f985687 c990923 c990922))

1. (~ (c (f985687 c990923 c990922) c990923))
2. (~ (c c990923 (f985687 c990923 c990922)))
3. (~ (c c990923 c990922))
4. (o c990923 c990922)

> ((c X X) <--)


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c996264 c996263)) v (pp c996264 c996263))


> hypdisj
=============================
Step 3

? (pp c996264 c996263)

1. (tpp c996264 c996263)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c996264 c996263)

1. (~ (pp c996264 c996263))
2. (tpp c996264 c996263)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c1001661 c1001660)) v (p c1001661 c1001660))


> hypdisj
=============================
Step 3

? (p c1001661 c1001660)

1. (pp c1001661 c1001660)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c1001661 c1001660)

1. (~ (p c1001661 c1001660))
2. (pp c1001661 c1001660)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c1007116 c1007115)) v (~ (c c1007114 c1007116))) v (c c1007114 c1007115))


> hypdisj
=============================
Step 3

? (c c1007114 c1007115)

1. (c c1007114 c1007116)
2. (p c1007116 c1007115)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c1007115)
|
|1. (~ (c c1007114 c1007115))
|2. (c c1007114 c1007116)
|3. (p c1007116 c1007115)
|
|> hyp
=============================
Step 5

? (c c1007114 c1007116)

1. (~ (c c1007114 c1007115))
2. (c c1007114 c1007116)
3. (p c1007116 c1007115)

> hyp


LEMMA

From po(x,y) and tpp(y,z), x is connected to z.
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp y z)) => (c x z)))))


> revsk
=============================
Step 2

? (((~ (po c1012727 c1012726)) v (~ (tpp c1012726 c1012725))) v (c c1012727 c1012725))


> hypdisj
=============================
Step 3

? (c c1012727 c1012725)

1. (tpp c1012726 c1012725)
2. (po c1012727 c1012726)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var32 c1012725)
|
|1. (~ (c c1012727 c1012725))
|2. (tpp c1012726 c1012725)
|3. (po c1012727 c1012726)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 5
|
|? (pp Var32 c1012725)
|
|1. (~ (p Var32 c1012725))
|2. (~ (c c1012727 c1012725))
|3. (tpp c1012726 c1012725)
|4. (po c1012727 c1012726)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 6
|
|? (tpp Var32 c1012725)
|
|1. (~ (pp Var32 c1012725))
|2. (~ (p Var32 c1012725))
|3. (~ (c c1012727 c1012725))
|4. (tpp c1012726 c1012725)
|5. (po c1012727 c1012726)
|
|> hyp
=============================
Step 7

? (c c1012727 c1012726)

1. (~ (c c1012727 c1012725))
2. (tpp c1012726 c1012725)
3. (po c1012727 c1012726)

> ((c X Y) <-- (o X Y))
=============================
Step 8

? (o c1012727 c1012726)

1. (~ (c c1012727 c1012726))
2. (~ (c c1012727 c1012725))
3. (tpp c1012726 c1012725)
4. (po c1012727 c1012726)

> ((o X Y) <-- (po X Y))
=============================
Step 9

? (po c1012727 c1012726)

1. (~ (o c1012727 c1012726))
2. (~ (c c1012727 c1012726))
3. (~ (c c1012727 c1012725))
4. (tpp c1012726 c1012725)
5. (po c1012727 c1012726)

> hyp


LEMMA

Classify x,z as ec or po or pp.
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp y z)) => ((ec x z) v ((po x z) v (pp x z)))))))


> revsk
=============================
Step 2

? (((~ (po c1018494 c1018493)) v (~ (tpp c1018493 c1018492))) v ((ec c1018494 c1018492) v ((po c1018494 c1018492) v (pp c1018494 c1018492))))


> hypdisj
=============================
Step 3

? (pp c1018494 c1018492)

1. (~ (po c1018494 c1018492))
2. (~ (ec c1018494 c1018492))
3. (tpp c1018493 c1018492)
4. (po c1018494 c1018493)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c1018494 c1018492)
|
|1. (~ (pp c1018494 c1018492))
|2. (~ (po c1018494 c1018492))
|3. (~ (ec c1018494 c1018492))
|4. (tpp c1018493 c1018492)
|5. (po c1018494 c1018493)
|
|> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
|||=============================
|||Step 5
|||
|||? (o c1018494 c1018492)
|||
|||1. (~ (p c1018494 c1018492))
|||2. (~ (pp c1018494 c1018492))
|||3. (~ (po c1018494 c1018492))
|||4. (~ (ec c1018494 c1018492))
|||5. (tpp c1018493 c1018492)
|||6. (po c1018494 c1018493)
|||
|||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
||||=============================
||||Step 6
||||
||||? (c c1018494 c1018492)
||||
||||1. (~ (o c1018494 c1018492))
||||2. (~ (p c1018494 c1018492))
||||3. (~ (pp c1018494 c1018492))
||||4. (~ (po c1018494 c1018492))
||||5. (~ (ec c1018494 c1018492))
||||6. (tpp c1018493 c1018492)
||||7. (po c1018494 c1018493)
||||
||||> ((c X Z) <-- (po X Y) (tpp Y Z))
|||||=============================
|||||Step 7
|||||
|||||? (po c1018494 Var67)
|||||
|||||1. (~ (c c1018494 c1018492))
|||||2. (~ (o c1018494 c1018492))
|||||3. (~ (p c1018494 c1018492))
|||||4. (~ (pp c1018494 c1018492))
|||||5. (~ (po c1018494 c1018492))
|||||6. (~ (ec c1018494 c1018492))
|||||7. (tpp c1018493 c1018492)
|||||8. (po c1018494 c1018493)
|||||
|||||> hyp
||||=============================
||||Step 8
||||
||||? (tpp c1018493 c1018492)
||||
||||1. (~ (c c1018494 c1018492))
||||2. (~ (o c1018494 c1018492))
||||3. (~ (p c1018494 c1018492))
||||4. (~ (pp c1018494 c1018492))
||||5. (~ (po c1018494 c1018492))
||||6. (~ (ec c1018494 c1018492))
||||7. (tpp c1018493 c1018492)
||||8. (po c1018494 c1018493)
||||
||||> hyp
|||=============================
|||Step 9
|||
|||? (~ (ec c1018494 c1018492))
|||
|||1. (~ (o c1018494 c1018492))
|||2. (~ (p c1018494 c1018492))
|||3. (~ (pp c1018494 c1018492))
|||4. (~ (po c1018494 c1018492))
|||5. (~ (ec c1018494 c1018492))
|||6. (tpp c1018493 c1018492)
|||7. (po c1018494 c1018493)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (p c1018492 c1018494))
||
||1. (~ (p c1018494 c1018492))
||2. (~ (pp c1018494 c1018492))
||3. (~ (po c1018494 c1018492))
||4. (~ (ec c1018494 c1018492))
||5. (tpp c1018493 c1018492)
||6. (po c1018494 c1018493)
||
||> ((~ (p Z X)) <-- (po X Y) (tpp Y Z))
|||=============================
|||Step 11
|||
|||? (po c1018494 Var73)
|||
|||1. (p c1018492 c1018494)
|||2. (~ (p c1018494 c1018492))
|||3. (~ (pp c1018494 c1018492))
|||4. (~ (po c1018494 c1018492))
|||5. (~ (ec c1018494 c1018492))
|||6. (tpp c1018493 c1018492)
|||7. (po c1018494 c1018493)
|||
|||> hyp
||=============================
||Step 12
||
||? (tpp c1018493 c1018492)
||
||1. (p c1018492 c1018494)
||2. (~ (p c1018494 c1018492))
||3. (~ (pp c1018494 c1018492))
||4. (~ (po c1018494 c1018492))
||5. (~ (ec c1018494 c1018492))
||6. (tpp c1018493 c1018492)
||7. (po c1018494 c1018493)
||
||> hyp
|=============================
|Step 13
|
|? (~ (po c1018494 c1018492))
|
|1. (~ (p c1018494 c1018492))
|2. (~ (pp c1018494 c1018492))
|3. (~ (po c1018494 c1018492))
|4. (~ (ec c1018494 c1018492))
|5. (tpp c1018493 c1018492)
|6. (po c1018494 c1018493)
|
|> hyp
=============================
Step 14

? (~ (p c1018492 c1018494))

1. (~ (pp c1018494 c1018492))
2. (~ (po c1018494 c1018492))
3. (~ (ec c1018494 c1018492))
4. (tpp c1018493 c1018492)
5. (po c1018494 c1018493)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 15
|
|? (c Var79 c1018492)
|
|1. (p c1018492 c1018494)
|2. (~ (pp c1018494 c1018492))
|3. (~ (po c1018494 c1018492))
|4. (~ (ec c1018494 c1018492))
|5. (tpp c1018493 c1018492)
|6. (po c1018494 c1018493)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 16
||
||? (p Var82 c1018492)
||
||1. (~ (c Var79 c1018492))
||2. (p c1018492 c1018494)
||3. (~ (pp c1018494 c1018492))
||4. (~ (po c1018494 c1018492))
||5. (~ (ec c1018494 c1018492))
||6. (tpp c1018493 c1018492)
||7. (po c1018494 c1018493)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 17
||
||? (pp Var82 c1018492)
||
||1. (~ (p Var82 c1018492))
||2. (~ (c Var79 c1018492))
||3. (p c1018492 c1018494)
||4. (~ (pp c1018494 c1018492))
||5. (~ (po c1018494 c1018492))
||6. (~ (ec c1018494 c1018492))
||7. (tpp c1018493 c1018492)
||8. (po c1018494 c1018493)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 18
||
||? (tpp Var82 c1018492)
||
||1. (~ (pp Var82 c1018492))
||2. (~ (p Var82 c1018492))
||3. (~ (c Var79 c1018492))
||4. (p c1018492 c1018494)
||5. (~ (pp c1018494 c1018492))
||6. (~ (po c1018494 c1018492))
||7. (~ (ec c1018494 c1018492))
||8. (tpp c1018493 c1018492)
||9. (po c1018494 c1018493)
||
||> hyp
|=============================
|Step 19
|
|? (c (f1012783 c1018493 Var91 Var92) c1018493)
|
|1. (~ (c (f1012783 c1018493 Var91 Var92) c1018492))
|2. (p c1018492 c1018494)
|3. (~ (pp c1018494 c1018492))
|4. (~ (po c1018494 c1018492))
|5. (~ (ec c1018494 c1018492))
|6. (tpp c1018493 c1018492)
|7. (po c1018494 c1018493)
|
|> ((c (f1012783 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 20
|
|? (~ (p c1018493 Var91))
|
|1. (~ (c (f1012783 c1018493 Var91 Var92) c1018493))
|2. (~ (c (f1012783 c1018493 Var91 Var92) c1018492))
|3. (p c1018492 c1018494)
|4. (~ (pp c1018494 c1018492))
|5. (~ (po c1018494 c1018492))
|6. (~ (ec c1018494 c1018492))
|7. (tpp c1018493 c1018492)
|8. (po c1018494 c1018493)
|
|> ((~ (p Y X)) <-- (po X Y))
|=============================
|Step 21
|
|? (po Var91 c1018493)
|
|1. (p c1018493 Var91)
|2. (~ (c (f1012783 c1018493 Var91 Var92) c1018493))
|3. (~ (c (f1012783 c1018493 Var91 Var92) c1018492))
|4. (p c1018492 c1018494)
|5. (~ (pp c1018494 c1018492))
|6. (~ (po c1018494 c1018492))
|7. (~ (ec c1018494 c1018492))
|8. (tpp c1018493 c1018492)
|9. (po c1018494 c1018493)
|
|> hyp
=============================
Step 22

? (~ (c (f1012783 c1018493 c1018494 Var92) c1018494))

1. (p c1018492 c1018494)
2. (~ (pp c1018494 c1018492))
3. (~ (po c1018494 c1018492))
4. (~ (ec c1018494 c1018492))
5. (tpp c1018493 c1018492)
6. (po c1018494 c1018493)

> ((~ (c (f1012783 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 23

? (~ (p c1018493 c1018494))

1. (c (f1012783 c1018493 c1018494 Var92) c1018494)
2. (p c1018492 c1018494)
3. (~ (pp c1018494 c1018492))
4. (~ (po c1018494 c1018492))
5. (~ (ec c1018494 c1018492))
6. (tpp c1018493 c1018492)
7. (po c1018494 c1018493)

> ((~ (p Y X)) <-- (po X Y))
=============================
Step 24

? (po c1018494 c1018493)

1. (p c1018493 c1018494)
2. (c (f1012783 c1018493 c1018494 Var92) c1018494)
3. (p c1018492 c1018494)
4. (~ (pp c1018494 c1018492))
5. (~ (po c1018494 c1018492))
6. (~ (ec c1018494 c1018492))
7. (tpp c1018493 c1018492)
8. (po c1018494 c1018493)

> hyp


LEMMA

The ec(x,z) branch is impossible under po(x,y) and tpp(y,z).
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp y z)) => (~ (ec x z))))))


> revsk
=============================
Step 2

? (((~ (po c1024677 c1024676)) v (~ (tpp c1024676 c1024675))) v (~ (ec c1024677 c1024675)))


> hypdisj
=============================
Step 3

? (~ (ec c1024677 c1024675))

1. (tpp c1024676 c1024675)
2. (po c1024677 c1024676)

> ((~ (ec X Y)) <-- (o X Y))
=============================
Step 4

? (o c1024677 c1024675)

1. (ec c1024677 c1024675)
2. (tpp c1024676 c1024675)
3. (po c1024677 c1024676)

> ((o X Z) <-- (p Y X) (p Y Z))
|=============================
|Step 5
|
|? (p Var64 c1024677)
|
|1. (~ (o c1024677 c1024675))
|2. (ec c1024677 c1024675)
|3. (tpp c1024676 c1024675)
|4. (po c1024677 c1024676)
|
|> ((p Z X) <-- (~ (c (f1018556 Z X Y) Z)))
|=============================
|Step 6
|
|? (~ (c (f1018556 Var64 c1024677 Var67) Var64))
|
|1. (~ (p Var64 c1024677))
|2. (~ (o c1024677 c1024675))
|3. (ec c1024677 c1024675)
|4. (tpp c1024676 c1024675)
|5. (po c1024677 c1024676)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 7
||
||? (p (f1018573 Var70 Var74) Var70)
||
||1. (c (f1018556 (f1018573 Var70 Var74) c1024677 Var67) (f1018573 Var70 Var74))
||2. (~ (p (f1018573 Var70 Var74) c1024677))
||3. (~ (o c1024677 c1024675))
||4. (ec c1024677 c1024675)
||5. (tpp c1024676 c1024675)
||6. (po c1024677 c1024676)
||
||> ((p (f1018573 X Y) X) <-- (o X Y))
||=============================
||Step 8
||
||? (o Var70 Var74)
||
||1. (~ (p (f1018573 Var70 Var74) Var70))
||2. (c (f1018556 (f1018573 Var70 Var74) c1024677 Var67) (f1018573 Var70 Var74))
||3. (~ (p (f1018573 Var70 Var74) c1024677))
||4. (~ (o c1024677 c1024675))
||5. (ec c1024677 c1024675)
||6. (tpp c1024676 c1024675)
||7. (po c1024677 c1024676)
||
||> ((o X Y) <-- (po X Y))
||=============================
||Step 9
||
||? (po Var70 Var74)
||
||1. (~ (o Var70 Var74))
||2. (~ (p (f1018573 Var70 Var74) Var70))
||3. (c (f1018556 (f1018573 Var70 Var74) c1024677 Var67) (f1018573 Var70 Var74))
||4. (~ (p (f1018573 Var70 Var74) c1024677))
||5. (~ (o c1024677 c1024675))
||6. (ec c1024677 c1024675)
||7. (tpp c1024676 c1024675)
||8. (po c1024677 c1024676)
||
||> hyp
|=============================
|Step 10
|
|? (~ (c (f1018556 (f1018573 c1024677 c1024676) c1024677 Var67) c1024677))
|
|1. (c (f1018556 (f1018573 c1024677 c1024676) c1024677 Var67) (f1018573 c1024677 c1024676))
|2. (~ (p (f1018573 c1024677 c1024676) c1024677))
|3. (~ (o c1024677 c1024675))
|4. (ec c1024677 c1024675)
|5. (tpp c1024676 c1024675)
|6. (po c1024677 c1024676)
|
|> ((~ (c (f1018556 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 11
|
|? (~ (p (f1018573 c1024677 c1024676) c1024677))
|
|1. (c (f1018556 (f1018573 c1024677 c1024676) c1024677 Var67) c1024677)
|2. (c (f1018556 (f1018573 c1024677 c1024676) c1024677 Var67) (f1018573 c1024677 c1024676))
|3. (~ (p (f1018573 c1024677 c1024676) c1024677))
|4. (~ (o c1024677 c1024675))
|5. (ec c1024677 c1024675)
|6. (tpp c1024676 c1024675)
|7. (po c1024677 c1024676)
|
|> hyp
=============================
Step 12

? (p (f1018573 c1024677 c1024676) c1024675)

1. (~ (o c1024677 c1024675))
2. (ec c1024677 c1024675)
3. (tpp c1024676 c1024675)
4. (po c1024677 c1024676)

> ((p Z X) <-- (~ (c (f1018556 Z X Y) Z)))
=============================
Step 13

? (~ (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676)))

1. (~ (p (f1018573 c1024677 c1024676) c1024675))
2. (~ (o c1024677 c1024675))
3. (ec c1024677 c1024675)
4. (tpp c1024676 c1024675)
5. (po c1024677 c1024676)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 14
|
|? (p (f1018573 c1024677 c1024676) c1024676)
|
|1. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
|2. (~ (p (f1018573 c1024677 c1024676) c1024675))
|3. (~ (o c1024677 c1024675))
|4. (ec c1024677 c1024675)
|5. (tpp c1024676 c1024675)
|6. (po c1024677 c1024676)
|
|> ((p (f1018573 X Y) Y) <-- (o X Y))
|=============================
|Step 15
|
|? (o c1024677 c1024676)
|
|1. (~ (p (f1018573 c1024677 c1024676) c1024676))
|2. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
|3. (~ (p (f1018573 c1024677 c1024676) c1024675))
|4. (~ (o c1024677 c1024675))
|5. (ec c1024677 c1024675)
|6. (tpp c1024676 c1024675)
|7. (po c1024677 c1024676)
|
|> ((o X Y) <-- (po X Y))
|=============================
|Step 16
|
|? (po c1024677 c1024676)
|
|1. (~ (o c1024677 c1024676))
|2. (~ (p (f1018573 c1024677 c1024676) c1024676))
|3. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
|4. (~ (p (f1018573 c1024677 c1024676) c1024675))
|5. (~ (o c1024677 c1024675))
|6. (ec c1024677 c1024675)
|7. (tpp c1024676 c1024675)
|8. (po c1024677 c1024676)
|
|> hyp
=============================
Step 17

? (~ (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024676))

1. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
2. (~ (p (f1018573 c1024677 c1024676) c1024675))
3. (~ (o c1024677 c1024675))
4. (ec c1024677 c1024675)
5. (tpp c1024676 c1024675)
6. (po c1024677 c1024676)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 18
|
|? (p c1024676 Var94)
|
|1. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024676)
|2. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
|3. (~ (p (f1018573 c1024677 c1024676) c1024675))
|4. (~ (o c1024677 c1024675))
|5. (ec c1024677 c1024675)
|6. (tpp c1024676 c1024675)
|7. (po c1024677 c1024676)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 19
|
|? (pp c1024676 Var94)
|
|1. (~ (p c1024676 Var94))
|2. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024676)
|3. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
|4. (~ (p (f1018573 c1024677 c1024676) c1024675))
|5. (~ (o c1024677 c1024675))
|6. (ec c1024677 c1024675)
|7. (tpp c1024676 c1024675)
|8. (po c1024677 c1024676)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 20
|
|? (tpp c1024676 Var94)
|
|1. (~ (pp c1024676 Var94))
|2. (~ (p c1024676 Var94))
|3. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024676)
|4. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
|5. (~ (p (f1018573 c1024677 c1024676) c1024675))
|6. (~ (o c1024677 c1024675))
|7. (ec c1024677 c1024675)
|8. (tpp c1024676 c1024675)
|9. (po c1024677 c1024676)
|
|> hyp
=============================
Step 21

? (~ (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024675))

1. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024676)
2. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
3. (~ (p (f1018573 c1024677 c1024676) c1024675))
4. (~ (o c1024677 c1024675))
5. (ec c1024677 c1024675)
6. (tpp c1024676 c1024675)
7. (po c1024677 c1024676)

> ((~ (c (f1018556 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 22

? (~ (p (f1018573 c1024677 c1024676) c1024675))

1. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024675)
2. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) c1024676)
3. (c (f1018556 (f1018573 c1024677 c1024676) c1024675 Var83) (f1018573 c1024677 c1024676))
4. (~ (p (f1018573 c1024677 c1024676) c1024675))
5. (~ (o c1024677 c1024675))
6. (ec c1024677 c1024675)
7. (tpp c1024676 c1024675)
8. (po c1024677 c1024676)

> hyp


LEMMA

Proper part splits into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c1031014 c1031013)) v ((tpp c1031014 c1031013) v (ntpp c1031014 c1031013)))


> hypdisj
=============================
Step 3

? (ntpp c1031014 c1031013)

1. (~ (tpp c1031014 c1031013))
2. (pp c1031014 c1031013)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f1024794 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c1031014 c1031013)
|
|1. (~ (ntpp c1031014 c1031013))
|2. (~ (tpp c1031014 c1031013))
|3. (pp c1031014 c1031013)
|
|> hyp
=============================
Step 5

? (~ (ec (f1024794 c1031014 c1031013 Var32) c1031014))

1. (~ (ntpp c1031014 c1031013))
2. (~ (tpp c1031014 c1031013))
3. (pp c1031014 c1031013)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c1031014 Var36)
||
||1. (ec (f1024794 c1031014 c1031013 Var32) c1031014)
||2. (~ (ntpp c1031014 c1031013))
||3. (~ (tpp c1031014 c1031013))
||4. (pp c1031014 c1031013)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f1024794 c1031014 c1031013 Var32) c1031013)
|
|1. (ec (f1024794 c1031014 c1031013 Var32) c1031014)
|2. (~ (ntpp c1031014 c1031013))
|3. (~ (tpp c1031014 c1031013))
|4. (pp c1031014 c1031013)
|
|> ((ec (f1024794 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c1031014 c1031013))
||
||1. (~ (ec (f1024794 c1031014 c1031013 Var32) c1031013))
||2. (ec (f1024794 c1031014 c1031013 Var32) c1031014)
||3. (~ (ntpp c1031014 c1031013))
||4. (~ (tpp c1031014 c1031013))
||5. (pp c1031014 c1031013)
||
||> hyp
|=============================
|Step 9
|
|? (pp c1031014 c1031013)
|
|1. (~ (ec (f1024794 c1031014 c1031013 Var32) c1031013))
|2. (ec (f1024794 c1031014 c1031013 Var32) c1031014)
|3. (~ (ntpp c1031014 c1031013))
|4. (~ (tpp c1031014 c1031013))
|5. (pp c1031014 c1031013)
|
|> hyp
=============================
Step 10

? (~ (tpp c1031014 c1031013))

1. (ec (f1024794 c1031014 c1031013 Var32) c1031014)
2. (~ (ntpp c1031014 c1031013))
3. (~ (tpp c1031014 c1031013))
4. (pp c1031014 c1031013)

> hyp


LEMMA

Use Lemma8 and eliminate ec with Lemma9. Then split pp into tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((po x y) & (tpp y z)) => (((po x z) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (po c1037504 c1037503)) v (~ (tpp c1037503 c1037502))) v (((po c1037504 c1037502) v (tpp c1037504 c1037502)) v (ntpp c1037504 c1037502)))


> hypdisj
=============================
Step 3

? (ntpp c1037504 c1037502)

1. (~ (tpp c1037504 c1037502))
2. (~ (po c1037504 c1037502))
3. (tpp c1037503 c1037502)
4. (po c1037504 c1037503)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c1037504 c1037502)
|
|1. (~ (ntpp c1037504 c1037502))
|2. (~ (tpp c1037504 c1037502))
|3. (~ (po c1037504 c1037502))
|4. (tpp c1037503 c1037502)
|5. (po c1037504 c1037503)
|
|> ((pp Y Z) <-- (po Y X) (tpp X Z) (~ (ec Y Z)) (~ (po Y Z)))
||||=============================
||||Step 5
||||
||||? (po c1037504 Var35)
||||
||||1. (~ (pp c1037504 c1037502))
||||2. (~ (ntpp c1037504 c1037502))
||||3. (~ (tpp c1037504 c1037502))
||||4. (~ (po c1037504 c1037502))
||||5. (tpp c1037503 c1037502)
||||6. (po c1037504 c1037503)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (tpp c1037503 c1037502)
|||
|||1. (~ (pp c1037504 c1037502))
|||2. (~ (ntpp c1037504 c1037502))
|||3. (~ (tpp c1037504 c1037502))
|||4. (~ (po c1037504 c1037502))
|||5. (tpp c1037503 c1037502)
|||6. (po c1037504 c1037503)
|||
|||> hyp
||=============================
||Step 7
||
||? (~ (ec c1037504 c1037502))
||
||1. (~ (pp c1037504 c1037502))
||2. (~ (ntpp c1037504 c1037502))
||3. (~ (tpp c1037504 c1037502))
||4. (~ (po c1037504 c1037502))
||5. (tpp c1037503 c1037502)
||6. (po c1037504 c1037503)
||
||> ((~ (ec X Z)) <-- (po X Y) (tpp Y Z))
|||=============================
|||Step 8
|||
|||? (po c1037504 Var40)
|||
|||1. (ec c1037504 c1037502)
|||2. (~ (pp c1037504 c1037502))
|||3. (~ (ntpp c1037504 c1037502))
|||4. (~ (tpp c1037504 c1037502))
|||5. (~ (po c1037504 c1037502))
|||6. (tpp c1037503 c1037502)
|||7. (po c1037504 c1037503)
|||
|||> hyp
||=============================
||Step 9
||
||? (tpp c1037503 c1037502)
||
||1. (ec c1037504 c1037502)
||2. (~ (pp c1037504 c1037502))
||3. (~ (ntpp c1037504 c1037502))
||4. (~ (tpp c1037504 c1037502))
||5. (~ (po c1037504 c1037502))
||6. (tpp c1037503 c1037502)
||7. (po c1037504 c1037503)
||
||> hyp
|=============================
|Step 10
|
|? (~ (po c1037504 c1037502))
|
|1. (~ (pp c1037504 c1037502))
|2. (~ (ntpp c1037504 c1037502))
|3. (~ (tpp c1037504 c1037502))
|4. (~ (po c1037504 c1037502))
|5. (tpp c1037503 c1037502)
|6. (po c1037504 c1037503)
|
|> hyp
=============================
Step 11

? (~ (tpp c1037504 c1037502))

1. (~ (ntpp c1037504 c1037502))
2. (~ (tpp c1037504 c1037502))
3. (~ (po c1037504 c1037502))
4. (tpp c1037503 c1037502)
5. (po c1037504 c1037503)

> hyp
